COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00005 ENDMK
C⊗;


(DEFPROP INSTFNS
 (NIL COMMUTATIVE INST ISVAR SUBLIS COMMINST ASSOCINST)
VALUE)

(DEFPROP COMMUTATIVE
 (LAMBDA (OP) (MEMBER OP (QUOTE (PLUS TIMES UNION INTERSECTION))))
EXPR)

(DEFPROP INST
 (LAMBDA(E M P)
  (COND	((EQ P (QUOTE NO)) P)
	((ATOM M)
	 (COND ((ISVAR M)
		((LAMBDA (W) (COND ((NULL W) (CONS (CONS M E) P)) ((EQUAL (CDR W) E) P) (T (QUOTE NO))))
		 (ASSOC M P)))
	       ((EQ M E) P)
	       (T (QUOTE NO))))
	((ATOM E) (QUOTE NO))
	((COMMUTATIVE (CAR M))
	 (COND ((ATOM E) (QUOTE NO)) (T (COMMINST (CDR E) (CDR M) (INST (CAR E) (CAR M) P) NIL))))
	(T (INST (CDR E) (CDR M) (INST (CAR E) (CAR M) P)))))
EXPR)

(DEFPROP ISVAR
 (LAMBDA (M) (MEMBER M (QUOTE (U V W X Y Z))))
EXPR)

(DEFPROP SUBLIS
 (LAMBDA(E P)
  (COND	((ATOM E) ((LAMBDA (W) (COND ((NULL W) E) (T (CDR W)))) (ASSOC E P)))
	(T
	 ((LAMBDA (X Y) (COND ((AND (EQ X (CAR E)) (EQ Y (CDR E))) E) (T (CONS X Y))))
	  (SUBLIS (CAR E) P)
	  (SUBLIS (CDR E) P)))))
EXPR)

(DEFPROP COMMINST
 (LAMBDA(LEXP LPAT A U)
  (COND	((EQ A (QUOTE NO)) (QUOTE NO))
	((ATOM LPAT)
	 (COND ((ISVAR LPAT)
		((LAMBDA(W)
		  (COND	((NULL W) (CONS (CONS LPAT (APPEND LEXP U)) A))
			((AND (EQUAL (CDR W) LEXP) (NULL U)) A)
			(T (QUOTE NO))))
		 (ASSOC LPAT A)))
	       ((EQ LPAT LEXP) A)
	       (T (QUOTE NO))))
	((NULL LEXP) (QUOTE NO))
	(T
	 ((LAMBDA(W)
	   (COND ((EQ W (QUOTE NO)) (COMMINST (CDR LEXP) LPAT A (CONS (CAR LEXP) U)))

		(T ((LAMBDA (Z) (COND ((EQ Z @NO) (COMMINST (CDR LEXP) LPAT A
(CONS (CAR LEXP) U))) (T Z)))


		(COMMINST (APPEND U (CDR LEXP)) (CDR LPAT) W NIL)))))
	  (INST (CAR LEXP) (CAR LPAT) A)))))
EXPR)